Nuprl Lemma : es-rcv-atom_wf
11,40
postcript
pdf
es
:ES,
a
:Atom1,
e
:E.
e
receives ||
a
latex
Definitions
e
receives ||
a
,
P
Q
,
x
:
A
B
(
x
)
,
,
Type
,
b
,
isrcv(
e
)
,
x
:
T
||
a
,
valtype(
e
)
,
val(
e
)
,
E
,
x
:
A
.
B
(
x
)
,
Atom$n
,
t
T
,
ES
Lemmas
event
system
wf
,
es-E
wf
,
es-val
wf
,
es-valtype
wf
,
free-from-atom
wf1
,
es-isrcv
wf
,
assert
wf
origin
es:ES, a:Atom1, e:E. e receives || a 
es:ES, a:Atom1, e:E. e receives || a 
Q
B(x)
bx:A. B(x) T